Nuprl Definition : ecl_ind
11,40
ecl_ind(
x
;
ecl_ind(
k
,
test
.
base
(
k
;
test
);
ecl_ind(
a
,
b
,
rec1
,
rec2
.
seq
(
a
;
b
;
rec1
;
rec2
);
ecl_ind(
a
,
b
,
rec1
,
rec2
.
and
(
a
;
b
;
rec1
;
rec2
);
ecl_ind(
a
,
b
,
rec1
,
rec2
.
or
(
a
;
b
;
rec1
;
rec2
);
ecl_ind(
a
,
rec1
.
repeat
(
a
;
rec1
);
ecl_ind(
a
,
n
,
rec1
.
act
(
a
;
n
;
rec1
);
ecl_ind(
a
,
n
,
rec1
.
throw
(
a
;
n
;
rec1
);
ecl_ind(
a
,
l
,
rec1
.
catch
(
a
;
l
;
rec1
))
== case
x
==
of inl(
x
) =>
base
(
x
.1;
x
.2)
== o
| inr(
x
) => case
x
== o| inr(
x
) =>
of inl(
x
) =>
seq
(
x
.1
== o| inr(
x
) => of inl(
x
) =>
seq
;
x
.2
== o| inr(
x
) => of inl(
x
) =>
seq
;ecl_ind((
x
.1);
== o| inr(
x
) => of inl(
x
) =>
seq
;ecl_ind(
k
,
test
.
base
(
k
;
test
);
== o| inr(
x
) => of inl(
x
) =>
seq
;ecl_ind(
a
,
b
,
rec1
,
rec2
.
seq
(
a
;
b
;
rec1
;
rec2
);
== o| inr(
x
) => of inl(
x
) =>
seq
;ecl_ind(
a
,
b
,
rec1
,
rec2
.
and
(
a
;
b
;
rec1
;
rec2
);
== o| inr(
x
) => of inl(
x
) =>
seq
;ecl_ind(
a
,
b
,
rec1
,
rec2
.
or
(
a
;
b
;
rec1
;
rec2
);
== o| inr(
x
) => of inl(
x
) =>
seq
;ecl_ind(
a
,
rec1
.
repeat
(
a
;
rec1
);
== o| inr(
x
) => of inl(
x
) =>
seq
;ecl_ind(
a
,
n
,
rec1
.
act
(
a
;
n
;
rec1
);
== o| inr(
x
) => of inl(
x
) =>
seq
;ecl_ind(
a
,
n
,
rec1
.
throw
(
a
;
n
;
rec1
);
== o| inr(
x
) => of inl(
x
) =>
seq
;ecl_ind(
a
,
l
,
rec1
.
catch
(
a
;
l
;
rec1
))
== o| inr(
x
) => of inl(
x
) =>
seq
;ecl_ind((
x
.2);
== o| inr(
x
) => of inl(
x
) =>
seq
;ecl_ind(
k
,
test
.
base
(
k
;
test
);
== o| inr(
x
) => of inl(
x
) =>
seq
;ecl_ind(
a
,
b
,
rec1
,
rec2
.
seq
(
a
;
b
;
rec1
;
rec2
);
== o| inr(
x
) => of inl(
x
) =>
seq
;ecl_ind(
a
,
b
,
rec1
,
rec2
.
and
(
a
;
b
;
rec1
;
rec2
);
== o| inr(
x
) => of inl(
x
) =>
seq
;ecl_ind(
a
,
b
,
rec1
,
rec2
.
or
(
a
;
b
;
rec1
;
rec2
);
== o| inr(
x
) => of inl(
x
) =>
seq
;ecl_ind(
a
,
rec1
.
repeat
(
a
;
rec1
);
== o| inr(
x
) => of inl(
x
) =>
seq
;ecl_ind(
a
,
n
,
rec1
.
act
(
a
;
n
;
rec1
);
== o| inr(
x
) => of inl(
x
) =>
seq
;ecl_ind(
a
,
n
,
rec1
.
throw
(
a
;
n
;
rec1
);
== o| inr(
x
) => of inl(
x
) =>
seq
;ecl_ind(
a
,
l
,
rec1
.
catch
(
a
;
l
;
rec1
)))
== o| inr(
x
) => o
| inr(
x
) => case
x
== o| inr(
x
) => o| inr(
x
) =>
of inl(
x
) =>
and
(
x
.1
== o| inr(
x
) => o| inr(
x
) => of inl(
x
) =>
and
;
x
.2
== o| inr(
x
) => o| inr(
x
) => of inl(
x
) =>
and
;ecl_ind((
x
.1);
== o| inr(
x
) => o| inr(
x
) => of inl(
x
) =>
and
;ecl_ind(
k
,
test
.
base
(
k
;
test
);
== o| inr(
x
) => o| inr(
x
) => of inl(
x
) =>
and
;ecl_ind(
a
,
b
,
rec1
,
rec2
.
seq
(
a
;
b
;
rec1
;
rec2
);
== o| inr(
x
) => o| inr(
x
) => of inl(
x
) =>
and
;ecl_ind(
a
,
b
,
rec1
,
rec2
.
and
(
a
;
b
;
rec1
;
rec2
);
== o| inr(
x
) => o| inr(
x
) => of inl(
x
) =>
and
;ecl_ind(
a
,
b
,
rec1
,
rec2
.
or
(
a
;
b
;
rec1
;
rec2
);
== o| inr(
x
) => o| inr(
x
) => of inl(
x
) =>
and
;ecl_ind(
a
,
rec1
.
repeat
(
a
;
rec1
);
== o| inr(
x
) => o| inr(
x
) => of inl(
x
) =>
and
;ecl_ind(
a
,
n
,
rec1
.
act
(
a
;
n
;
rec1
);
== o| inr(
x
) => o| inr(
x
) => of inl(
x
) =>
and
;ecl_ind(
a
,
n
,
rec1
.
throw
(
a
;
n
;
rec1
);
== o| inr(
x
) => o| inr(
x
) => of inl(
x
) =>
and
;ecl_ind(
a
,
l
,
rec1
.
catch
(
a
;
l
;
rec1
))
== o| inr(
x
) => o| inr(
x
) => of inl(
x
) =>
and
;ecl_ind((
x
.2);
== o| inr(
x
) => o| inr(
x
) => of inl(
x
) =>
and
;ecl_ind(
k
,
test
.
base
(
k
;
test
);
== o| inr(
x
) => o| inr(
x
) => of inl(
x
) =>
and
;ecl_ind(
a
,
b
,
rec1
,
rec2
.
seq
(
a
;
b
;
rec1
;
rec2
);
== o| inr(
x
) => o| inr(
x
) => of inl(
x
) =>
and
;ecl_ind(
a
,
b
,
rec1
,
rec2
.
and
(
a
;
b
;
rec1
;
rec2
);
== o| inr(
x
) => o| inr(
x
) => of inl(
x
) =>
and
;ecl_ind(
a
,
b
,
rec1
,
rec2
.
or
(
a
;
b
;
rec1
;
rec2
);
== o| inr(
x
) => o| inr(
x
) => of inl(
x
) =>
and
;ecl_ind(
a
,
rec1
.
repeat
(
a
;
rec1
);
== o| inr(
x
) => o| inr(
x
) => of inl(
x
) =>
and
;ecl_ind(
a
,
n
,
rec1
.
act
(
a
;
n
;
rec1
);
== o| inr(
x
) => o| inr(
x
) => of inl(
x
) =>
and
;ecl_ind(
a
,
n
,
rec1
.
throw
(
a
;
n
;
rec1
);
== o| inr(
x
) => o| inr(
x
) => of inl(
x
) =>
and
;ecl_ind(
a
,
l
,
rec1
.
catch
(
a
;
l
;
rec1
)))
== o| inr(
x
) => o| inr(
x
) => o
| inr(
x
) => case
x
== o| inr(
x
) => o| inr(
x
) => o| inr(
x
) =>
of inl(
x
) =>
or
(
x
.1
== o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => of inl(
x
) =>
or
;
x
.2
== o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => of inl(
x
) =>
or
;ecl_ind((
x
.1);
== o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => of inl(
x
) =>
or
;ecl_ind(
k
,
test
.
base
(
k
;
test
);
== o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => of inl(
x
) =>
or
;ecl_ind(
a
,
b
,
rec1
,
rec2
.
seq
(
a
;
b
;
rec1
;
rec2
);
== o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => of inl(
x
) =>
or
;ecl_ind(
a
,
b
,
rec1
,
rec2
.
and
(
a
;
b
;
rec1
;
rec2
);
== o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => of inl(
x
) =>
or
;ecl_ind(
a
,
b
,
rec1
,
rec2
.
or
(
a
;
b
;
rec1
;
rec2
);
== o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => of inl(
x
) =>
or
;ecl_ind(
a
,
rec1
.
repeat
(
a
;
rec1
);
== o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => of inl(
x
) =>
or
;ecl_ind(
a
,
n
,
rec1
.
act
(
a
;
n
;
rec1
);
== o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => of inl(
x
) =>
or
;ecl_ind(
a
,
n
,
rec1
.
throw
(
a
;
n
;
rec1
);
== o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => of inl(
x
) =>
or
;ecl_ind(
a
,
l
,
rec1
.
catch
(
a
;
l
;
rec1
))
== o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => of inl(
x
) =>
or
;ecl_ind((
x
.2);
== o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => of inl(
x
) =>
or
;ecl_ind(
k
,
test
.
base
(
k
;
test
);
== o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => of inl(
x
) =>
or
;ecl_ind(
a
,
b
,
rec1
,
rec2
.
seq
(
a
;
b
;
rec1
;
rec2
);
== o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => of inl(
x
) =>
or
;ecl_ind(
a
,
b
,
rec1
,
rec2
.
and
(
a
;
b
;
rec1
;
rec2
);
== o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => of inl(
x
) =>
or
;ecl_ind(
a
,
b
,
rec1
,
rec2
.
or
(
a
;
b
;
rec1
;
rec2
);
== o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => of inl(
x
) =>
or
;ecl_ind(
a
,
rec1
.
repeat
(
a
;
rec1
);
== o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => of inl(
x
) =>
or
;ecl_ind(
a
,
n
,
rec1
.
act
(
a
;
n
;
rec1
);
== o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => of inl(
x
) =>
or
;ecl_ind(
a
,
n
,
rec1
.
throw
(
a
;
n
;
rec1
);
== o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => of inl(
x
) =>
or
;ecl_ind(
a
,
l
,
rec1
.
catch
(
a
;
l
;
rec1
)))
== o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o
| inr(
x
) => case
x
== o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) =>
of inl(
x
) =>
repeat
(
x
== o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => of inl(
x
) =>
repeat
;ecl_ind
== o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => of inl(
x
) =>
repeat
(
x
;
== o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => of inl(
x
) =>
repeat
(
k
,
test
.
base
(
k
;
test
);
== o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => of inl(
x
) =>
repeat
(
a
,
b
,
rec1
,
rec2
.
seq
(
a
== o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => of inl(
x
) =>
repeat
(
a
,
b
,
rec1
,
rec2
.
seq
;
b
== o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => of inl(
x
) =>
repeat
(
a
,
b
,
rec1
,
rec2
.
seq
;
rec1
== o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => of inl(
x
) =>
repeat
(
a
,
b
,
rec1
,
rec2
.
seq
;
rec2
);
== o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => of inl(
x
) =>
repeat
(
a
,
b
,
rec1
,
rec2
.
and
(
a
== o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => of inl(
x
) =>
repeat
(
a
,
b
,
rec1
,
rec2
.
and
;
b
== o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => of inl(
x
) =>
repeat
(
a
,
b
,
rec1
,
rec2
.
and
;
rec1
== o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => of inl(
x
) =>
repeat
(
a
,
b
,
rec1
,
rec2
.
and
;
rec2
);
== o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => of inl(
x
) =>
repeat
(
a
,
b
,
rec1
,
rec2
.
or
(
a
== o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => of inl(
x
) =>
repeat
(
a
,
b
,
rec1
,
rec2
.
or
;
b
== o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => of inl(
x
) =>
repeat
(
a
,
b
,
rec1
,
rec2
.
or
;
rec1
== o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => of inl(
x
) =>
repeat
(
a
,
b
,
rec1
,
rec2
.
or
;
rec2
);
== o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => of inl(
x
) =>
repeat
(
a
,
rec1
.
repeat
(
a
;
rec1
);
== o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => of inl(
x
) =>
repeat
(
a
,
n
,
rec1
.
act
(
a
;
n
;
rec1
);
== o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => of inl(
x
) =>
repeat
(
a
,
n
,
rec1
.
throw
(
a
;
n
;
rec1
);
== o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => of inl(
x
) =>
repeat
(
a
,
l
,
rec1
.
catch
(
a
;
l
;
rec1
)
== o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => of inl(
x
) =>
repeat
(
))
== o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o
| inr(
x
) => case
x
== o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) =>
of inl(
x
) =>
act
(
x
.1
== o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => of inl(
x
) =>
act
;
x
.2
== o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => of inl(
x
) =>
act
;ecl_ind
== o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => of inl(
x
) =>
act
((
x
.1);
== o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => of inl(
x
) =>
act
(
k
,
test
.
base
(
k
== o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => of inl(
x
) =>
act
(
k
,
test
.
base
;
test
);
== o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => of inl(
x
) =>
act
(
a
,
b
,
rec1
,
rec2
.
seq
(
a
== o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => of inl(
x
) =>
act
(
a
,
b
,
rec1
,
rec2
.
seq
;
b
== o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => of inl(
x
) =>
act
(
a
,
b
,
rec1
,
rec2
.
seq
;
rec1
== o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => of inl(
x
) =>
act
(
a
,
b
,
rec1
,
rec2
.
seq
;
rec2
);
== o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => of inl(
x
) =>
act
(
a
,
b
,
rec1
,
rec2
.
and
(
a
== o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => of inl(
x
) =>
act
(
a
,
b
,
rec1
,
rec2
.
and
;
b
== o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => of inl(
x
) =>
act
(
a
,
b
,
rec1
,
rec2
.
and
;
rec1
== o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => of inl(
x
) =>
act
(
a
,
b
,
rec1
,
rec2
.
and
;
rec2
);
== o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => of inl(
x
) =>
act
(
a
,
b
,
rec1
,
rec2
.
or
(
a
== o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => of inl(
x
) =>
act
(
a
,
b
,
rec1
,
rec2
.
or
;
b
== o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => of inl(
x
) =>
act
(
a
,
b
,
rec1
,
rec2
.
or
;
rec1
== o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => of inl(
x
) =>
act
(
a
,
b
,
rec1
,
rec2
.
or
;
rec2
);
== o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => of inl(
x
) =>
act
(
a
,
rec1
.
repeat
(
a
== o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => of inl(
x
) =>
act
(
a
,
rec1
.
repeat
;
rec1
);
== o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => of inl(
x
) =>
act
(
a
,
n
,
rec1
.
act
(
a
== o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => of inl(
x
) =>
act
(
a
,
n
,
rec1
.
act
;
n
== o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => of inl(
x
) =>
act
(
a
,
n
,
rec1
.
act
;
rec1
);
== o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => of inl(
x
) =>
act
(
a
,
n
,
rec1
.
throw
(
a
== o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => of inl(
x
) =>
act
(
a
,
n
,
rec1
.
throw
;
n
== o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => of inl(
x
) =>
act
(
a
,
n
,
rec1
.
throw
;
rec1
);
== o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => of inl(
x
) =>
act
(
a
,
l
,
rec1
.
catch
(
a
== o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => of inl(
x
) =>
act
(
a
,
l
,
rec1
.
catch
;
l
== o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => of inl(
x
) =>
act
(
a
,
l
,
rec1
.
catch
;
rec1
)
== o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => of inl(
x
) =>
act
(
))
== o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o
| inr(
x
) => case
x
== o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) =>
of inl(
x
) =>
throw
(
x
.1
== o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => of inl(
x
) =>
throw
;
x
.2
== o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => of inl(
x
) =>
throw
;ecl_ind
== o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => of inl(
x
) =>
throw
((
x
.1);
== o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => of inl(
x
) =>
throw
(
k
,
test
.
base
(
k
== o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => of inl(
x
) =>
throw
(
k
,
test
.
base
;
test
);
== o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => of inl(
x
) =>
throw
(
a
,
b
,
rec1
,
rec2
.
seq
(
a
== o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => of inl(
x
) =>
throw
(
a
,
b
,
rec1
,
rec2
.
seq
;
b
== o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => of inl(
x
) =>
throw
(
a
,
b
,
rec1
,
rec2
.
seq
;
rec1
== o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => of inl(
x
) =>
throw
(
a
,
b
,
rec1
,
rec2
.
seq
;
rec2
);
== o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => of inl(
x
) =>
throw
(
a
,
b
,
rec1
,
rec2
.
and
(
a
== o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => of inl(
x
) =>
throw
(
a
,
b
,
rec1
,
rec2
.
and
;
b
== o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => of inl(
x
) =>
throw
(
a
,
b
,
rec1
,
rec2
.
and
;
rec1
== o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => of inl(
x
) =>
throw
(
a
,
b
,
rec1
,
rec2
.
and
;
rec2
);
== o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => of inl(
x
) =>
throw
(
a
,
b
,
rec1
,
rec2
.
or
(
a
== o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => of inl(
x
) =>
throw
(
a
,
b
,
rec1
,
rec2
.
or
;
b
== o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => of inl(
x
) =>
throw
(
a
,
b
,
rec1
,
rec2
.
or
;
rec1
== o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => of inl(
x
) =>
throw
(
a
,
b
,
rec1
,
rec2
.
or
;
rec2
);
== o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => of inl(
x
) =>
throw
(
a
,
rec1
.
repeat
(
a
== o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => of inl(
x
) =>
throw
(
a
,
rec1
.
repeat
;
rec1
);
== o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => of inl(
x
) =>
throw
(
a
,
n
,
rec1
.
act
(
a
== o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => of inl(
x
) =>
throw
(
a
,
n
,
rec1
.
act
;
n
== o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => of inl(
x
) =>
throw
(
a
,
n
,
rec1
.
act
;
rec1
);
== o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => of inl(
x
) =>
throw
(
a
,
n
,
rec1
.
throw
(
a
== o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => of inl(
x
) =>
throw
(
a
,
n
,
rec1
.
throw
;
n
== o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => of inl(
x
) =>
throw
(
a
,
n
,
rec1
.
throw
;
rec1
);
== o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => of inl(
x
) =>
throw
(
a
,
l
,
rec1
.
catch
(
a
== o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => of inl(
x
) =>
throw
(
a
,
l
,
rec1
.
catch
;
l
== o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => of inl(
x
) =>
throw
(
a
,
l
,
rec1
.
catch
;
rec1
)
== o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => of inl(
x
) =>
throw
(
))
== o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o
| inr(
x
) =>
catch
(
x
.1
== o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) =>
catch
;
x
.2
== o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) =>
catch
;ecl_ind
== o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) =>
catch
((
x
.1);
== o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) =>
catch
(
k
,
test
.
base
(
k
== o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) =>
catch
(
k
,
test
.
base
;
test
);
== o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) =>
catch
(
a
,
b
,
rec1
,
rec2
.
seq
(
a
== o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) =>
catch
(
a
,
b
,
rec1
,
rec2
.
seq
;
b
== o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) =>
catch
(
a
,
b
,
rec1
,
rec2
.
seq
;
rec1
== o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) =>
catch
(
a
,
b
,
rec1
,
rec2
.
seq
;
rec2
);
== o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) =>
catch
(
a
,
b
,
rec1
,
rec2
.
and
(
a
== o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) =>
catch
(
a
,
b
,
rec1
,
rec2
.
and
;
b
== o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) =>
catch
(
a
,
b
,
rec1
,
rec2
.
and
;
rec1
== o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) =>
catch
(
a
,
b
,
rec1
,
rec2
.
and
;
rec2
);
== o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) =>
catch
(
a
,
b
,
rec1
,
rec2
.
or
(
a
== o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) =>
catch
(
a
,
b
,
rec1
,
rec2
.
or
;
b
== o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) =>
catch
(
a
,
b
,
rec1
,
rec2
.
or
;
rec1
== o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) =>
catch
(
a
,
b
,
rec1
,
rec2
.
or
;
rec2
);
== o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) =>
catch
(
a
,
rec1
.
repeat
(
a
== o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) =>
catch
(
a
,
rec1
.
repeat
;
rec1
);
== o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) =>
catch
(
a
,
n
,
rec1
.
act
(
a
== o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) =>
catch
(
a
,
n
,
rec1
.
act
;
n
== o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) =>
catch
(
a
,
n
,
rec1
.
act
;
rec1
);
== o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) =>
catch
(
a
,
n
,
rec1
.
throw
(
a
== o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) =>
catch
(
a
,
n
,
rec1
.
throw
;
n
== o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) =>
catch
(
a
,
n
,
rec1
.
throw
;
rec1
);
== o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) =>
catch
(
a
,
l
,
rec1
.
catch
(
a
== o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) =>
catch
(
a
,
l
,
rec1
.
catch
;
l
== o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) =>
catch
(
a
,
l
,
rec1
.
catch
;
rec1
)
== o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) =>
catch
(
))
(recursive)
latex
Definitions
Y
,
x
.
A
(
x
)
,
case
b
of inl(
x
) =>
s
(
x
) | inr(
y
) =>
t
(
y
)
,
t
.2
,
f
(
a
)
,
t
.1
FDL editor aliases
ecl_ind, ecl_ind
origin
x.A(x)x.A(x)